Replace use of deprecated nil_typet in java_type_from_string [blocks: #3800] #3929

tautschnig · 2019-01-24T22:59:24Z

Use typet or optionalt. ~~Do not review just yet, I will split this up in several commit as it touches way too many parts of the codebase in a single commit.~~

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 4aad8d1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98657901
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 152dfcc).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98710526
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

peterschrammel · 2019-01-28T23:03:43Z

jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp

          // NOLINTNEXTLINE(whitespace/braces)
          symbol_exprt generic_param{
            "specalisedGeneric",
-            java_type_from_string("LDummyGeneric<Ljava/lang/Interger;>;")};
+            *java_type_from_string("LDummyGeneric<Ljava/lang/Interger;>;")};


❓ Is Interger intended here (and below)?

I guess it doesn't matter? db6756e - @thk123 ?

I guess not...! Will have a detailed look at this test, but of course no more or less broken than it was before.

peterschrammel · 2019-01-28T23:05:23Z

jbmc/src/java_bytecode/java_types.cpp

@@ -582,26 +582,25 @@ typet java_type_from_string(
        std::back_inserter(parameters),
        [](const typet &type) { return java_method_typet::parametert(type); });

-      return java_method_typet(std::move(parameters), std::move(return_type));
+      return java_method_typet(std::move(parameters), std::move(*return_type));


Are we sure this has a value?

I have no idea, but it was previously used without any sanity check, so I'd now rely on operator* failing an assertion...

peterschrammel · 2019-01-28T23:05:52Z

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

-      f.descriptor,
-      f.signature,
-      id2string(class_symbol.name));
+    field_type = *java_type_from_string_with_exception(


Are we sure this has a value? (and other places)

As above: no idea, but it was previously used unchecked. There are a couple of places that failed this while running the regression tests, and those I have now guarded appropriately. I still think that this makes optionalt<typet> much better as at least you'd have a failing assertion instead of silently passing around a nil_typet that some later stage won't know how to deal with.

thk123

Will create a manual bump for this.

thk123 · 2019-01-31T10:06:13Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

    std::ostringstream id_oss;
    id_oss << method_id << "::" << v.name;
    irep_idt identifier(id_oss.str());
-    symbol_exprt result(identifier, t);
+    symbol_exprt result = symbol_exprt::typeless(identifier);


❓ This change looks a little suspicious? Previously the type of the symbol was derived from the signature or descriptor, now is a typeless identifier?

The type was sometimes nil_typet() (because trying to derive the type failed) and nobody noticed, because really the type of this is never used.

In that case could I suggest using an irep_idt instead of a symbol_exprt? Otherwise someone will surely assume that variables[n].type() is a sensible thing to look at.

That would necessitate some refactoring of this code as the expression is also used to communicate ID_C_base_name.

thk123 · 2019-01-31T10:06:39Z

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -548,8 +548,8 @@ void java_bytecode_parsert::get_class_refs()

    case CONSTANT_NameAndType:
      {
-        typet t=java_type_from_string(id2string(pool_entry(c.ref2).s));
-        get_class_refs_rec(t);
+        const auto t = java_type_from_string(id2string(pool_entry(c.ref2).s));


⛏️ while in the area, t -> type

I just got rid of it, it didn't carry much value...

thk123 · 2019-01-31T10:08:30Z

jbmc/src/java_bytecode/java_bytecode_parser.cpp

-    else
-      method_type=java_type_from_string(method.descriptor);
+    else if(const auto method_type = java_type_from_string(method.descriptor))
+      get_class_refs_rec(*method_type);


💡 Might be worth sticking a warning here that it somehow failed to get the type from both the signature and the descriptor. I'd even be tempted to put an UNREACHABLE; here, but I suppose this is one of the cases you were referring to where this broke tests.

Indeed, this is reachable/reached in several regression tests. I don't feel sufficiently competent on this code to assess whether that's actually a problem. Any volunteers?

I put UNREACHABLE; here and didn't get any failures in jbmc* - have a specific example? (will try the other two places too).

Not sure what exactly your change was, but I'd just use else { typet method_type = *java_type_from_string(method.descriptor); get_class_refs_rec(method_type); } here.

thk123 · 2019-01-31T10:08:57Z

jbmc/src/java_bytecode/java_bytecode_parser.cpp

-        var_type=java_type_from_string(var.descriptor);
-      get_class_refs_rec(var_type);
+      else if(const auto var_type = java_type_from_string(var.descriptor))
+        get_class_refs_rec(*var_type);


💡 Again - some kind of warning in the else case makes sense here I think. 🔥

thk123 · 2019-01-31T10:30:20Z

jbmc/src/java_bytecode/java_bytecode_parser.cpp

-    get_class_refs_rec(value_type);
+    const auto value_type = java_type_from_string(id2string(value_id));
+    if(value_type.has_value())
+      get_class_refs_rec(*value_type);


thk123 · 2019-01-31T10:39:10Z

jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp

          // NOLINTNEXTLINE(whitespace/braces)
          symbol_exprt generic_param{
            "specalisedGeneric",
-            java_type_from_string("LDummyGeneric<Ljava/lang/Interger;>;")};
+            *java_type_from_string("LDummyGeneric<Ljava/lang/Interger;>;")};


I guess not...! Will have a detailed look at this test, but of course no more or less broken than it was before.

tautschnig · 2019-01-31T10:56:48Z

I have rebased this one. @thk123 or anyone else (@smowton ?) who feels comfortable with the Java bytecode parser: the cases where I'm now silently skipping calls to get_class_refs_rec may be worth exploring as highlighted by @thk123 above. They are easily triggered via the regression test suite.

thk123 · 2019-01-31T11:12:58Z

I will have a look and see whether this looks like a real concern or not.

smowton · 2019-01-31T11:15:30Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

-      INVARIANT(member_type_from_signature.id()==ID_code, "Must be code type");
+      auto member_type_from_signature =
+        java_type_from_string(signature.value(), class_name);
+      INVARIANT(


I'd actually delete this, we're about to check both those things by deref'ing and casting

smowton · 2019-01-31T11:17:26Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

    std::ostringstream id_oss;
    id_oss << method_id << "::" << v.name;
    irep_idt identifier(id_oss.str());
-    symbol_exprt result(identifier, t);
+    symbol_exprt result = symbol_exprt::typeless(identifier);


In that case could I suggest using an irep_idt instead of a symbol_exprt? Otherwise someone will surely assume that variables[n].type() is a sensible thing to look at.

smowton · 2019-01-31T11:25:08Z

@tautschnig it's unsurprising with our known-to-be-broken generic signature parsing sometimes bails with nil_typet (we should probably treat that the same as the exception thrown when we find something we can't handle and fall back to the descriptor). If that happens with a descriptor (non-generic type) then I'm pretty surprised.

thk123

This breaks TG (both a trivial compile error and a failing test) I'm investigating now.

thk123 · 2019-01-31T13:01:38Z

Now waiting on CI - in the mean time will investigate the above optional returns.

tautschnig · 2019-01-31T13:05:24Z

Thank you @thk123 !

thk123 · 2019-01-31T13:58:03Z

@tautschnig I've made tautschnig#12 which tightens these to not allow the descriptor to fail (I could only find one failing test - and the problem was the test). Happy for you to fold that into this PR or get this one merged and then I'll raise that as a new PR.

(TG bump is based at this PR and is still running, but passed some tests locally).

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: c523d5f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99277071
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

tautschnig · 2019-01-31T14:04:52Z

@thk123 PR merged in here and the entire branch rebased onto latest develop, you might want to update the TG bump to use this?

Use optionalt<typet> as recommended in the deprecation note.

The jasmin contained two errors: calling base class constructor with invokevirtual rather than invokespecial the descriptor of the type for the local variable was not a valid descriptor.

There should be no unsupported cases here.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 8f71a23).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99300653
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

thk123 · 2019-02-01T10:14:09Z

TG bump passing.

tautschnig added cleanup work in progress blocker labels Jan 24, 2019

tautschnig self-assigned this Jan 24, 2019

tautschnig requested review from allredj, cesaro, chrisr-diffblue, cristina-david, kroening, martin-cs, NathanJPhillips, peterschrammel, pkesseli, romainbrenguier, smowton and thk123 as code owners January 24, 2019 22:59

tautschnig force-pushed the deprecation-nil_typet branch from af40105 to e4cffb5 Compare January 25, 2019 12:39

tautschnig removed the work in progress label Jan 25, 2019

tautschnig assigned tautschnig and unassigned tautschnig Jan 25, 2019

tautschnig force-pushed the deprecation-nil_typet branch from e4cffb5 to 4e6d256 Compare January 25, 2019 12:45

tautschnig changed the title ~~Replace all uses of deprecated nil_typet [blocks: #3800]~~ Replace use of deprecated nil_typet in java_type_from_string [blocks: #3800] Jan 25, 2019

tautschnig assigned smowton, thk123 and peterschrammel and unassigned tautschnig Jan 25, 2019

tautschnig force-pushed the deprecation-nil_typet branch from 4e6d256 to 4aad8d1 Compare January 25, 2019 17:16

allredj reviewed Jan 25, 2019

View reviewed changes

tautschnig force-pushed the deprecation-nil_typet branch from 4aad8d1 to 152dfcc Compare January 26, 2019 13:14

allredj reviewed Jan 26, 2019

View reviewed changes

tautschnig assigned allredj Jan 26, 2019

peterschrammel reviewed Jan 28, 2019

View reviewed changes

thk123 reviewed Jan 31, 2019

View reviewed changes

tautschnig force-pushed the deprecation-nil_typet branch from 152dfcc to c523d5f Compare January 31, 2019 10:53

smowton reviewed Jan 31, 2019

View reviewed changes

thk123 suggested changes Jan 31, 2019

View reviewed changes

thk123 mentioned this pull request Jan 31, 2019

Tighten the changes to java bytecode parser tautschnig/cbmc#12

Merged

allredj reviewed Jan 31, 2019

View reviewed changes

tautschnig force-pushed the deprecation-nil_typet branch from d1bcbec to adf6c12 Compare January 31, 2019 14:04

tautschnig and others added 3 commits January 31, 2019 14:05

Replace use of deprecated nil_typet in java_type_from_string

08276eb

Use optionalt<typet> as recommended in the deprecation note.

Address errors in handcrafted bytecode

6f1084e

The jasmin contained two errors: calling base class constructor with invokevirtual rather than invokespecial the descriptor of the type for the local variable was not a valid descriptor.

Do not allow getting type from descriptor to fail

8f71a23

There should be no unsupported cases here.

tautschnig force-pushed the deprecation-nil_typet branch from adf6c12 to 8f71a23 Compare January 31, 2019 14:06

allredj reviewed Jan 31, 2019

View reviewed changes

thk123 approved these changes Feb 1, 2019

View reviewed changes

tautschnig merged commit 0e6538a into diffblue:develop Feb 1, 2019

tautschnig deleted the deprecation-nil_typet branch February 1, 2019 10:28

Replace use of deprecated nil_typet in java_type_from_string [blocks: #3800] #3929

Replace use of deprecated nil_typet in java_type_from_string [blocks: #3800] #3929

Uh oh!

Conversation

tautschnig commented Jan 24, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Jan 31, 2019

Uh oh!

thk123 commented Jan 31, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton commented Jan 31, 2019

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

thk123 commented Jan 31, 2019

Uh oh!

tautschnig commented Jan 31, 2019

Uh oh!

thk123 commented Jan 31, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Jan 31, 2019

tautschnig commented Jan 24, 2019 •

edited

Loading

thk123 commented Jan 31, 2019 •

edited

Loading